Nuprl Lemma : map_swap
4,23
postcript
pdf
A
,
B
:Type,
f
:(
B
A
),
x
:
B
List,
i
,
j
:
||
x
||. map(
f
;swap(
x
;
i
;
j
)) = swap(map(
f
;
x
);
i
;
j
)
A
List
latex
Definitions
x
:
A
.
B
(
x
)
,
i
j
,
||
as
||
,
(
i
,
j
)
,
{
i
..
j
}
,
,
t
T
,
P
Q
,
False
,
A
,
A
B
,
P
&
Q
,
i
j
<
k
,
P
Q
,
P
Q
,
map(
f
;
as
)
,
swap(
L
;
i
;
j
)
,
l
[
i
]
,
Prop
Lemmas
int
seg
wf
,
list
extensionality
,
map
wf
,
nat
wf
,
swap
select
,
map
select
,
select
wf
,
swap
wf
,
swap
length
,
map
length
,
le
wf
,
length
wf1
,
flip
wf
,
non
neg
length
origin
A, B:Type, f:(B
A), x:B List, i, j:
||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j) 
A List A, B:Type, f:(BA), x:B List, i, j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j) A List x:A. B(x)
j
} T
Q
A
B j < k
Q Q